$\forall$${\it Cmd}$:Type, $P$:(chain\_sys(${\it Cmd}$)$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$${\it cmd}$:${\it Cmd}$. $P$(csinput(${\it cmd}$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it from}$:Id, ${\it cmds}$:(${\it Cmd}$ List). $P$(csupdate(${\it from}$;${\it cmds}$)))
\\[0ex]$\Rightarrow$ \{$\forall$$x$:chain\_sys(${\it Cmd}$). $P$($x$)\}